T:Type, L:T List, P1, P2, Q1, Q2:(||L||Prop), R1, R2:(||L||||L||Prop).
(i:||L||. P1(i)  P2(i))
 (i:||L||. Q2(i)  Q1(i))
 (i, j:||L||. R1(i,j)  R2(i,j))
 causal_order(L;R1;P1;Q1)
 causal_order(L;R2;P2;Q2) 

latex

Definitions	P  Q, x:A. B(x), t  T, ||as||, False, A, AB, P & Q, i  j < k, {i..j}, Prop, x:A. B(x), causal_order(L;R;P;Q)
Lemmas	int seg wf, length wf1, le wf